Nuprl Definition : ma-compatible-decls
11,40
postcript
pdf
M1
||decl
M2
==
M1
.1 ||
M2
.1 & (
M1
.2).1 || (
M2
.2).1
latex
clarification:
ma-compatible-decls{i:l}
ma-compatible-decls
(
M1
;
M2
)
== fpf-compatible(Id;
x
.Type{i}; IdDeq; (
M1
.1); (
M2
.1))
==
& fpf-compatible(Knd;
x
.Type{i}; KindDeq; ((
M1
.2).1); ((
M2
.2).1))
latex
Definitions
P
&
Q
,
Id
,
IdDeq
,
f
||
g
,
Knd
,
Type
,
KindDeq
,
t
.1
,
t
.2
FDL editor aliases
ma-compatible-decls
origin